1. Technical Field
Disclosed embodiments related to computerized systems, computer-implemented methods, and computer-readable media. In particular, disclosed embodiments relate to verifying an access-control policy with arithmetic quantifier-free form constraints.
2. Description of the Related Art
Computer systems often implement access-control policies to prevent certain operations from taking place or to allow other operations to take place. For example, as is known in the art, a network firewall may filter incoming and/or outgoing network packets, such as IP packets for example. The firewall may allow some incoming packets to pass through the firewall and may block other packets from passing through. The firewall may rely on an access-control policy, which includes rules, to determine which packets to allow and which packets to block.
The firewall may use the rules to evaluate an operation vector, which may be a series of values defining an operation. For example, an operation vector may define each incoming packet. In a firewall, the operation vector may be values in a header of an incoming IP packet, such as source address and destination address. A rule from the access-control policy may be applied to the operation vector of the IP packet. If the values of the operation vector satisfy the rules, then the firewall may allow the operation by permitting the IP packet to pass.
The rules may be expressed in a language or in some format, and may express constraints on one or more fields of an operation vector. For example, an access-control policy rule in a firewall may be:[1,3,4,6,deny]  Equation 1
Each of 1, 3, 4, and 6 in Equation 1 may represent a different IP address, and “deny” may represent the operation of denying or blocking a packet through the firewall. The rule in Equation 1 indicates that if the source address of the operation vector is in the range between 1 and 3, and the destination address of the operation vector is in the range between 4 and 6, then the firewall should “deny” the IP packet and block it from passing through the firewall. This rule may be applied to an operation vector, which includes both the source address and the destination address of an IP packet header of the incoming IP packet. For example, the operation vector may be:[2,5]  Equation 2
The value of 2 may be the source address of the IP packet, and the value of 5 may be the destination address of the IP packet. The firewall may apply the constraint in the rule of Equation 1 to the operation vector of Equation 2. Specifically, the firewall may determine that the source address of the IP packet 2 is within the range 1-3, and may determine that the destination address of the IP packet 5 is in the range of 4-6. Accordingly, in this example, the values in the operation vector of Equation 2 meet the constraints in the rule of Equation 1, and therefore, the firewall denies the IP packet in accordance with the “deny” value in the fifth field of Equation 1, by blocking the IP packet from passing through the firewall.
Access-control policies may be used in other contexts, in addition to firewalls. For example, in operating systems, access-control policies may allow or prevent an object from writing to or reading from another object. Specifically, the operating system may implement a multi-level security (MLS) scheme to assign different security levels to different objects. This access-control policy may prevent specific interactions between certain objects, based on the security levels associated with the objects. One of ordinary skill will recognize that the use of “objects” herein is not restrictive, one or more other computing constructs may be used, such as processes, threads, files, instantiated classes, etc.
Accordingly, this access-control policy may include rules governing writing and reading among objects of different security levels. For example, an access-control policy rule in an MLS operating system may be:[read write,target security−subject security<2]  Equation 3
The first field in Equation 3 (“read write”) may represent operations associated with the access-control policy rule. And the second field in Equation 3 may represent a constraint on an operation vector that must be true for the operations in the first field to be executable. In this example, Equation 3 states that in order for a subject object to write to or read from a target object, the target object must be less than two security levels greater than the subject object's security level (i.e., target security−subject security<2). Such a rule may be useful in MLS operating systems to prevent a relatively unsecured object from accessing protected data associated with an object two or more security levels higher.
Similar to firewalls, operations between objects in an MLS operating system environment may also be defined by operation vectors. As discussed, an operation vector may be a series of values defining an operation. In the firewall example, the operation vector comprised the source and destination values in the incoming IP packet header. In the exemplary MLS operation system environment, however, the operation vector may be a series of values describing a write or read between two objects, such as[Object0,0,Object2,2,read]  Equation 4
The operation vector in Equation 4 describes an operation in which a subject Object0 with a security level 0 seeks to read from a target Object2 with a security level of 2. An operating system may apply the access-control policy rule of Equation 3 to the operation vector of Equation 4. By doing so, the operating system would determine that, counter to the requirement in Equation 3, the security level (2) of the target object (Object2), is not less than two security levels greater than the security level (0) of the subject object (Object0). In fact, Object2 is exactly two security levels higher than Object0. Accordingly, the access-control policy rule in Equation 3 would not be satisfied when applied to operation vector in Equation 3, and the operating system would deny the operation.
This is further illustrated in FIG. 1. FIG. 1 illustrates an operating system environment 100 implementing a MLS access-control policy among objects. Environment 100 includes different security levels: Security Level 0 (102), Security Level 1 (104), and Security Level 2 (106). As denoted in Equation 3, for a subject object to read from or write to a target object, the target object must be less than two security levels greater than the subject object's security level.
Environment 100 further includes Object0 108 at Security Level 0 and Object2 110 at Security Level 2. Because Object2 110 is at a higher security level than Object0 108, environment 100 permits Object2 110 to read from Object0 108, as indicated by operation 112, and also permits Object2 110 to write to Object0 108, as indicated by operation 114. And because Object0 108 is two security level lower than Object2 110, environment 100 prevents Object0 108 from reading from Object2 110, as indicated by operation 116, and also prevents Object0 108 from writing to Object2 110, as indicated by operation 118. Operation 116 illustrates the access-control policy rule of Equation 3 applied to the operation vector in Equation 4.
In this way, exemplary operating system environment 100 may enforce MLS access-control rules, such as Equation 3, for operations among objects at different security levels.
While the access-control policies discussed so far in the firewall example and the operation system example in FIG. 1 are straightforward, access-control policies may be extremely complex, and may include thousands of different rules. Therefore, a single operation vector may be evaluated by thousands of different rules to determine whether or not it is permitted or denied.
Moreover, an access-control policy can be viewed or represented as a large or complex constraint on values of some operation vector. Sometimes, it may be necessary to evaluate an access-control policy against other constraints. For example, it may be necessary to compare an access-control policy with some other constraint, to see if the operations prevented/denied by the constraint are also prevented/denied by the access-control policy. As another example, it may be necessary to compare two access-control policies to determine any differences among them. These evaluations may be challenging, given the complexities and sizes of access-control policies and/or constraints.
Prior art solutions attempted to compare two sets of constraints such as access-control policies or other types of constraints. In particular, the prior art solutions identified a set of operations denied by one constraint, which are permitted by another constraint, such as an access-control policy.
FIG. 2 illustrates a Venn diagram space 200 of constraints, which may be compared by prior art solutions. Space 200 includes a set 202 representing Constraint 1, which may be an access-control policy for a firewall, operating system, or other computing platform. Constraint 1 may be represented by rules in some format or language. In this example, the area inside set 202 may represent operations prevented by Constraint 1, while the area outside set 202 may represent operations allowed by Constraint 1.
Space 200 may also include set 204 representing Constraint 2, which may be an access-control policy, or any other constraint. Constraint 2 may also be represented by rules. The area inside set 204 may represent operations prevented by Constraint 2, while the area outside set 202 may represent operations allowed by Constraint 2. Space 200 may also include set 206 representing Constraint 3, which may be an access-control policy, or any other constraint. Constraint 3 may also be represented by rules. The area inside set 206 may represent operations prevented by Constraint 3, while the area outside set 206 may represent operations allowed by Constraint 3.
Alternatively, the area inside a set may represent operations allowed by a corresponding constraint, while the area outside a set may represent operations denied by the corresponding constraint, as understood to one of ordinary skill in the art.
It may be necessary to determine the extent to which the different constraints overlap. For example, a user may need to implement a constraint, such as Constraint 2 in association with Constraint 1. The user may need to determine if the operations prevented by Constraint 2 are already prevented by Constraint 1. As shown in FIG. 2, it is clear that set 202 of Constraint 1 subsumes set 204 of Constraint 2. In this example, this means that Constraint 1 prevents all operations that are also prevented by Constraint 2.
Similarly, a user may need to determine if the operations prevented by Constraint 3 are also prevented by Constraint 1. As shown in FIG. 2, it is clear that set 202 of Constraint 1 does not completely subsume set 206 of Constraint 3. This means that Constraint 1 prevents only some operations that are prevented by Constraint 3. Accordingly, the user would not be able to rely on Constraint 1 to fully enforce Constraint 3.
While the overlap among constraints is clear from FIG. 2, these determinations may practically be difficult to make, because the constraints are represented as complex series of rules. Accordingly, the prior art uses mathematical modeling to determine the extent to which a constraint subsumes another.
One prior art solution is described in “Modeling and Verification of IPSec and VPN Security Policies,” to Hamed et al. (2005). This solution is directed to verifying firewall access-control policies, specifically IPSec. The access-control policies are converted and represented as a collection of Boolean expressions. The prior art solution analyzes the access-control policies using ordered binary decision diagrams OBDD to determine the extent to which an access-control policy subsumes a constraint.
The drawback of this solution is that Boolean expressions are very low-level constructs. This may make it difficult to encode high level concepts such as constraints on processes, files, operations or packets, for example. This approach may also suffer from scalability problems. Indeed, because the Boolean expressions and OBDDs are low-level, the order of the Boolean expressions in the OBDD strongly affects the efficiency of the analysis. Therefore, when modeling complex policies or constraints, the increased size of the OBDDs may make it difficult to order the Binary expressions in the most efficient way. Moreover, this prior art solution only determines if one constraint subsumes another constraint. It does not provide multi-step verification, which allows verification of a sequence of operations.
Another prior art solution is described in “Automated Verification of Access Control Policies using a SAT Solver,” to Hughes et al. (2007). In this solution, access-control policies or other constraints are converted and formalized into XACML language, and then compiled into Boolean expressions. A SAT solver is used, by processing the Boolean expressions, to compare the constraints and determine the extent to which one constraint subsumes another.
The drawback of this solution is that the XACML language is very high-level and verbose for the purposes of modeling access-control policies. It has far greater expressive power than needed for most access-control policies. Accordingly, the translation of access-control policies into XACML may be computationally intensive. This solution also does not provide multi-step verification.
Accordingly, there is a need to express an access-control policy in a language that is more expressive and scalable than a Boolean expression, and also less verbose than XACML. It may also be necessary to provide multi-step verification of access-control policies.